EquivRel x,y:. x ~ y 

latex

Definitions	EquivRel x,y:T. E(x;y), Symmetrize(x,y.R(x;y);a;b), b | a, x,y. t(x;y), P  Q, x:A. B(x), t  T, a ~ b
Lemmas	divides wf, divides preorder, symmetrized preorder